#include <string.h>
#include "solver.h"

/* copy v1 to v2 */
void veci_copy2(veci *v1, veci *v2)
{
    v2->size = v1->size;
    v2->cap  = v1->cap;
    v2->ptr  = (int*)malloc(sizeof(int)*v1->cap);
    memcpy (v2->ptr, v1->ptr, sizeof(int)*v1->cap);
}

veci *veci_copy(veci *v)
{
    veci *v2 = (veci*)malloc(sizeof(veci));
    veci_copy2 (v, v2);
}

/* copy v1 to v2 */
void vecp_copy2(vecp *v1, vecp *v2)
{
    v2->size = v1->size;
    v2->cap  = v1->cap;
    v2->ptr  = (void**)malloc(sizeof(void*)*v1->cap);
}

struct clause_t
{
    int size_learnt;
    lit lits[0];
};

static inline int   clause_size       (clause* c)          { return c->size_learnt >> 1; }
static inline int   clause_learnt     (clause* c)          { return c->size_learnt & 1; }

clause *clause_copy(clause *v)
{
    int size, learnt;
    clause *v2;

    /*
    if (v == NULL)
    {
	return NULL;
    }
    */

    size            = clause_size (v);
    learnt          = clause_learnt (v);

    v2              = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));

    v2->size_learnt = v->size_learnt;
    memcpy (v2->lits, v->lits, sizeof(lit) * size + learnt * sizeof(float));

    return v2;
}

struct findclause_t {
    int idx;
    clause *p;
};
typedef struct findclause_t findclause;

int compare(findclause *p1, findclause *p2)
{
    if (p1->p > p2->p)
        return 1;
    else
        return 0;
}

findclause *init_findclause (solver *s)
{
    int i;
    findclause *p = (findclause*)malloc(sizeof(findclause)*s->clauses.size);

    for (i=0; i<s->clauses.size; i++)
    {
        p[i].idx = i;
	p[i].p   = s->clauses.ptr[i];
    }
    qsort (p, s->clauses.size, sizeof(findclause), compare);

    return p;
}

int do_findclause(findclause *p, int low, int high, clause *c)
{
    int med;

    med = (low + high) / 2;
    if (p[med].p == c)
	    return p[med].idx;
    else if (p[med].p > c)
	    return do_findclause(p,low,med-1,c);
    else
	    return do_findclause(p,med+1,high,c);
}

solver *solver_copy(solver *s)
{
    solver* s2 = (solver*)malloc(sizeof(solver));

    s2->size                   = s->size;
    s2->cap                    = s->cap;
    s2->qhead                  = s->qhead;
    s2->qtail                  = s->qtail;
    s2->var_inc                = s->var_inc;
    s2->var_decay              = s->var_decay;
    s2->cla_inc                = s->cla_inc;
    s2->cla_decay              = s->cla_decay;
    s2->root_level             = s->root_level;
    s2->simpdb_assigns         = s->simpdb_assigns;
    s2->simpdb_props           = s->simpdb_props;
    s2->random_seed            = s->random_seed;
    s2->progress_estimate      = s->progress_estimate;
    s2->verbosity              = s->verbosity;

    veci_copy2 (&s->tagged,    &s2->tagged);
    veci_copy2 (&s->stack,     &s2->stack);
    veci_copy2 (&s->order,     &s2->order);
    veci_copy2 (&s->trail_lim, &s2->trail_lim);
    veci_copy2 (&s->model,     &s2->model);

    s2->wlists    = (vecp*)   malloc(sizeof(vecp)*s->cap*2);
    s2->activity  = (double*) malloc(sizeof(double)*s->cap);
    s2->assigns   = (lbool*)  malloc(sizeof(lbool)*s->cap);
    s2->orderpos  = (int*)    malloc(sizeof(int)*s->cap);
    s2->reasons   = (clause**)malloc(sizeof(clause*)*s->cap);
    s2->levels    = (int*)    malloc(sizeof(int)*s->cap);
    s2->tags      = (lbool*)  malloc(sizeof(lbool)*s->cap);
    s2->trail     = (lit*)    malloc(sizeof(lit)*s->cap);

    memcpy (s2->activity, s->activity, sizeof(double)*s->cap);
    memcpy (s2->assigns, s->assigns, sizeof(lbool)*s->cap);
    memcpy (s2->orderpos, s->orderpos, sizeof(int)*s->cap);
    memcpy (s2->levels, s->levels, sizeof(int)*s->cap);
    memcpy (s2->tags, s->tags, sizeof(lbool)*s->cap);
    memcpy (s2->trail, s->trail, sizeof(lit)*s->cap);

    s2->binary = clause_copy (s->binary);

    memcpy (&s2->stats, &s->stats, sizeof (stats));

    int i,j;

    vecp_copy2 (&s->clauses,   &s2->clauses);
    for (i=0; i<s->clauses.size; i++)
    {
	s2->clauses.ptr[i] = clause_copy ((clause *)s->clauses.ptr[i]);
    }

    vecp_copy2 (&s->learnts,   &s2->learnts);
    for (i=0; i<s->learnts.size; i++)
    {
	s2->learnts.ptr[i] = veci_copy ((veci *)s->learnts.ptr[i]);
    }

    findclause *p;

    p = init_findclause (s);

    for (i=0; i<s->size*2; i++)
    {
        vecp_copy2 (&s->wlists[i], &s2->wlists[i]);
	for (j=0; j<s->wlists[i].size; j++)
	{
	    if (clause_is_lit(s->wlists[i].ptr[j]))
	    {
                s2->wlists[i].ptr[j] = s->wlists[i].ptr[j];
	    }
	    else
	    {
		s2->wlists[i].ptr[j] = s2->clauses.ptr[do_findclause(p,0,s->clauses.size-1,s->wlists[i].ptr[j])];
	    }
	}
    }

    free (p);

    return s2;
}
